the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E 

latex

Definitions

World, t  T, x:A. B(x), E, FairFifo, isrcv(k), sender(e), P  Q, time(e), kind(e), lnk(k), match(l;t;t'), b, , x:A. B(x), AB, P & Q, i  j < k, {x:A| B(x) }, x:AB(x), x:AB(x), #$n, {i..j}, Void, False, A, Id, Type, x. t(x), 2of(t), 1of(t), a(i;t), isnull(a), mu(f), source(l), <a,b>, S  T, {T}, x.A(x), IdLnk, s = t, n+m, snds(l;t), Msg, rcvs(l;t), destination(l), Action(i), a<b, Prop, i<j, ij, p  q, P  Q, w.M, mlnk(m), type List, Msg(M), m(i;t), onlnk(l;mss), ||as||,

Lemmas

w-m wf, Msg wf, w-onlnk wf, mlnk wf, w-M wf, iff transitivity, assert of band, and functionality wrt iff, assert of le int, assert of lt int, band wf, le int wf, lt int wf, w-action wf, ldst wf, w-rcvs wf, length wf1, w-Msg wf, w-snds wf, IdLnk wf, mu-property, lsrc wf, mu wf, not wf, w-isnull wf, w-a wf, pi1 wf, pi2 wf, nat wf, Id wf, w-match-exists, le wf, w-match wf, lnk wf, w-time wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, w-E wf, world wf